Nuprl Definition : fun_thru_2op 13,42
basic
FunThru2op(A;B;opa;opb;f) == a1, a2:A. f(a1 opa a2) = ((f(a1)) opb (f(a2))) 
latex

clarification:

basic
FunThru2op(A;B;opa;opb;f) == a1:A, a2:A. f(a1 opa a2) = ((f(a1)) opb (f(a2)))  B 
latex

Upgen algebra 1
Wellformedness Lemmasfun thru 2op wf
Definitionsx:A. B(x), x f y

origin